perm filename FILMAN.XGP[LET,JMC]3 blob
sn#412466 filedate 1979-01-23 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BASL30/FONT#1=BASI30/FONT#2=BASB30/FONT#10=BAXM30/FONT#11=ZERO30/FONT#3=STA200/FONT#4=NGB25
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305
␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ pJanuary 23, 1979
␈↓ ↓H␈↓Professor Jonathan L. Gross
␈↓ ↓H␈↓Department of Mathematical Statistics
␈↓ ↓H␈↓618 Mathematics
␈↓ ↓H␈↓Columbia University
␈↓ ↓H␈↓New York, New York 10027
␈↓ ↓H␈↓Dear Professor Gross:
␈↓ ↓H␈↓ Robert␈αFilman␈αhas␈αjust␈αcompleted␈αhis␈αPhD␈αdissertation␈αunder␈αmy␈αdirection,␈αand␈αit␈αis␈αin␈αthe
␈↓ ↓H␈↓hands␈α
of␈αthe␈α
readers.␈α He␈α
has␈α
just␈αpassed␈α
his␈α≡nal␈α
oral␈α
examination,␈αand␈α
I␈αexpect␈α
him␈αto␈α
complete
␈↓ ↓H␈↓all work for his PhD in Winter Quarter or Spring Quarter at the latest.
␈↓ ↓H␈↓ His␈αthesis␈α
opens␈αa␈α
new␈αpart␈αof␈α
the␈αepistemology␈α
of␈αarti≡cial␈α
intelligence␈α-␈αstudying␈α
reasoning
␈↓ ↓H␈↓that␈αcombines␈αinference␈αand␈αobservation.␈α To␈αmy␈αknowledge␈αthis␈αis␈αthe␈α≡rst␈αresearch␈αpaper␈αin␈αthe
␈↓ ↓H␈↓area.
␈↓ ↓H␈↓ Its␈αimportance␈α
comes␈αfrom␈αthe␈α
fact␈αthat␈αmuch␈α
human␈αreasoning␈αdoes␈α
not␈αfollow␈α
the␈αmodel
␈↓ ↓H␈↓of␈α⊃pure␈α⊃mathematics␈α⊃but␈α∩combines␈α⊃facts␈α⊃coming␈α⊃from␈α∩observation␈α⊃of␈α⊃the␈α⊃world␈α∩with␈α⊃general
␈↓ ↓H␈↓premises␈α∞-␈α∞here␈α∞expressed␈α
as␈α∞axioms.␈α∞ The␈α∞problem␈α∞chosen␈α
was␈α∞in␈α∞retrospective␈α∞chess␈α∞analysis␈α
-
␈↓ ↓H␈↓determining␈α
what␈α
piece␈α
fell␈α
o≥␈α∞the␈α
board␈α
in␈α
a␈α
chess␈α
position,␈α∞given␈α
that␈α
the␈α
position␈α
arose␈α∞in␈α
a
␈↓ ↓H␈↓legal␈α
game␈α
of␈α
chess.␈α
The␈αreasoning␈α
involved␈α
di≥ers␈α
in␈α
many␈αsubtle␈α
ways␈α
from␈α
that␈α
involved␈αin
␈↓ ↓H␈↓the proof of a mathematical theorem.
␈↓ ↓H␈↓ Filman␈αhas␈αdone␈αan␈αexcellent␈αjob␈αof␈αformalizing␈αthis␈αreasoning␈αto␈αthe␈αextent␈αthat␈αthe␈αproof
␈↓ ↓H␈↓can␈α∞be␈α∞generated␈α∂and␈α∞checked␈α∞using␈α∂FOL,␈α∞our␈α∞≡rst␈α∞order␈α∂logic␈α∞interactive␈α∞theorem␈α∂prover␈α∞and
␈↓ ↓H␈↓proof␈α
checker.␈α
In␈α
the␈α
course␈α
of␈α
this,␈αhe␈α
has␈α
made␈α
many␈α
improvements␈α
to␈α
FOL,␈α
necessitated␈αby␈α
the
␈↓ ↓H␈↓fact␈α⊃that␈α⊂this␈α⊃was␈α⊂the␈α⊃largest␈α⊂task␈α⊃undertaken␈α⊂with␈α⊃FOL␈α⊂and␈α⊃used␈α⊂many␈α⊃previously␈α⊂untested
␈↓ ↓H␈↓features.␈α⊃ He␈α∩has␈α⊃exhibited␈α∩a␈α⊃high␈α∩degree␈α⊃of␈α⊃originality␈α∩in␈α⊃deciding␈α∩how␈α⊃to␈α∩translate␈α⊃vague
␈↓ ↓H␈↓informal␈α↔concepts␈α↔into␈α↔a␈α↔precise␈α↔mathematical␈α↔formalism.␈α↔ The␈α↔work␈α↔also␈α_required␈α↔great
␈↓ ↓H␈↓perseverance,␈αand␈αFilman␈αhas␈αshown␈αit␈αin␈αcompleting␈αhis␈αthesis␈αless␈αthan␈αthree␈αyears␈αof␈αgraduate
␈↓ ↓H␈↓work at Stanford.
␈↓ ↓H␈↓αProfessor Jonathan L. Gross␈↓ ¬\January 23, 1979␈↓
nPage 2␈↓
␈↓ ↓H␈↓ Filman␈α∞has␈α∞given␈α
numerous␈α∞presentations␈α∞of␈α
his␈α∞work␈α∞and␈α
served␈α∞as␈α∞a␈α∞teaching␈α
assistant.
␈↓ ↓H␈↓His␈αoral␈αpresentation␈αis␈αalso␈αexcellent,␈αand␈αI␈αexpect␈αhim␈αto␈αbe␈αan␈αexcellent␈αteacher.␈α He␈αalso␈αhas␈αa
␈↓ ↓H␈↓co-operative and pleasant personality.
␈↓ ↓H␈↓Sincerely,
␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305
␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ pJanuary 23, 1979
␈↓ ↓H␈↓Prof. Paul W. Purdom, Jr.
␈↓ ↓H␈↓Chairman, Computer Science Department
␈↓ ↓H␈↓Lindley Hall 101
␈↓ ↓H␈↓Indiana University
␈↓ ↓H␈↓Bloomington, Indiana 47401
␈↓ ↓H␈↓Dear Professor Purdom:
␈↓ ↓H␈↓ Robert␈αFilman␈αhas␈αjust␈αcompleted␈αhis␈αPhD␈αdissertation␈αunder␈αmy␈αdirection,␈αand␈αit␈αis␈αin␈αthe
␈↓ ↓H␈↓hands␈α
of␈αthe␈α
readers.␈α He␈α
has␈α
just␈αpassed␈α
his␈α≡nal␈α
oral␈α
examination,␈αand␈α
I␈αexpect␈α
him␈αto␈α
complete
␈↓ ↓H␈↓all work for his PhD in Winter Quarter or Spring Quarter at the latest.
␈↓ ↓H␈↓ His␈αthesis␈α
opens␈αa␈α
new␈αpart␈αof␈α
the␈αepistemology␈α
of␈αarti≡cial␈α
intelligence␈α-␈αstudying␈α
reasoning
␈↓ ↓H␈↓that␈αcombines␈αinference␈αand␈αobservation.␈α To␈αmy␈αknowledge␈αthis␈αis␈αthe␈α≡rst␈αresearch␈αpaper␈αin␈αthe
␈↓ ↓H␈↓area.
␈↓ ↓H␈↓ Its␈αimportance␈α
comes␈αfrom␈αthe␈α
fact␈αthat␈αmuch␈α
human␈αreasoning␈αdoes␈α
not␈αfollow␈α
the␈αmodel
␈↓ ↓H␈↓of␈α⊃pure␈α⊃mathematics␈α⊃but␈α∩combines␈α⊃facts␈α⊃coming␈α⊃from␈α∩observation␈α⊃of␈α⊃the␈α⊃world␈α∩with␈α⊃general
␈↓ ↓H␈↓premises␈α∞-␈α∞here␈α∞expressed␈α
as␈α∞axioms.␈α∞ The␈α∞problem␈α∞chosen␈α
was␈α∞in␈α∞retrospective␈α∞chess␈α∞analysis␈α
-
␈↓ ↓H␈↓determining␈α
what␈α
piece␈α
fell␈α
o≥␈α∞the␈α
board␈α
in␈α
a␈α
chess␈α
position,␈α∞given␈α
that␈α
the␈α
position␈α
arose␈α∞in␈α
a
␈↓ ↓H␈↓legal␈α
game␈α
of␈α
chess.␈α
The␈αreasoning␈α
involved␈α
di≥ers␈α
in␈α
many␈αsubtle␈α
ways␈α
from␈α
that␈α
involved␈αin
␈↓ ↓H␈↓the proof of a mathematical theorem.
␈↓ ↓H␈↓ Filman␈αhas␈αdone␈αan␈αexcellent␈αjob␈αof␈αformalizing␈αthis␈αreasoning␈αto␈αthe␈αextent␈αthat␈αthe␈αproof
␈↓ ↓H␈↓can␈α∞be␈α∞generated␈α∂and␈α∞checked␈α∞using␈α∂FOL,␈α∞our␈α∞≡rst␈α∞order␈α∂logic␈α∞interactive␈α∞theorem␈α∂prover␈α∞and
␈↓ ↓H␈↓proof␈α
checker.␈α
In␈α
the␈α
course␈α
of␈α
this,␈αhe␈α
has␈α
made␈α
many␈α
improvements␈α
to␈α
FOL,␈α
necessitated␈αby␈α
the
␈↓ ↓H␈↓fact␈α⊃that␈α⊂this␈α⊃was␈α⊂the␈α⊃largest␈α⊂task␈α⊃undertaken␈α⊂with␈α⊃FOL␈α⊂and␈α⊃used␈α⊂many␈α⊃previously␈α⊂untested
␈↓ ↓H␈↓features.␈α⊃ He␈α∩has␈α⊃exhibited␈α∩a␈α⊃high␈α∩degree␈α⊃of␈α⊃originality␈α∩in␈α⊃deciding␈α∩how␈α⊃to␈α∩translate␈α⊃vague
␈↓ ↓H␈↓informal␈α↔concepts␈α↔into␈α↔a␈α↔precise␈α↔mathematical␈α↔formalism.␈α↔ The␈α↔work␈α↔also␈α_required␈α↔great
␈↓ ↓H␈↓perseverance,␈αand␈αFilman␈αhas␈αshown␈αit␈αin␈αcompleting␈αhis␈αthesis␈αless␈αthan␈αthree␈αyears␈αof␈αgraduate
␈↓ ↓H␈↓work at Stanford.
␈↓ ↓H␈↓αProf. Paul W. Purdom␈↓ ¬\January 23, 1979␈↓
nPage 2␈↓
␈↓ ↓H␈↓ Filman␈α∞has␈α∞given␈α
numerous␈α∞presentations␈α∞of␈α
his␈α∞work␈α∞and␈α
served␈α∞as␈α∞a␈α∞teaching␈α
assistant.
␈↓ ↓H␈↓His␈αoral␈αpresentation␈αis␈αalso␈αexcellent,␈αand␈αI␈αexpect␈αhim␈αto␈αbe␈αan␈αexcellent␈αteacher.␈α He␈αalso␈αhas␈αa
␈↓ ↓H␈↓co-operative and pleasant personality.
␈↓ ↓H␈↓Sincerely,
␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305
␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ pJanuary 23, 1979
␈↓ ↓H␈↓Prof. David Young, Jr.
␈↓ ↓H␈↓Chairman, Recruiting Committee
␈↓ ↓H␈↓Department of Computer Science
␈↓ ↓H␈↓University of Texas
␈↓ ↓H␈↓Austin, Texas 78712
␈↓ ↓H␈↓Dear Professor Young:
␈↓ ↓H␈↓ Robert␈αFilman␈αhas␈αjust␈αcompleted␈αhis␈αPhD␈αdissertation␈αunder␈αmy␈αdirection,␈αand␈αit␈αis␈αin␈αthe
␈↓ ↓H␈↓hands␈α
of␈αthe␈α
readers.␈α He␈α
has␈α
just␈αpassed␈α
his␈α≡nal␈α
oral␈α
examination,␈αand␈α
I␈αexpect␈α
him␈αto␈α
complete
␈↓ ↓H␈↓all work for his PhD in Winter Quarter or Spring Quarter at the latest.
␈↓ ↓H␈↓ His␈αthesis␈α
opens␈αa␈α
new␈αpart␈αof␈α
the␈αepistemology␈α
of␈αarti≡cial␈α
intelligence␈α-␈αstudying␈α
reasoning
␈↓ ↓H␈↓that␈αcombines␈αinference␈αand␈αobservation.␈α To␈αmy␈αknowledge␈αthis␈αis␈αthe␈α≡rst␈αresearch␈αpaper␈αin␈αthe
␈↓ ↓H␈↓area.
␈↓ ↓H␈↓ Its␈αimportance␈α
comes␈αfrom␈αthe␈α
fact␈αthat␈αmuch␈α
human␈αreasoning␈αdoes␈α
not␈αfollow␈α
the␈αmodel
␈↓ ↓H␈↓of␈α⊃pure␈α⊃mathematics␈α⊃but␈α∩combines␈α⊃facts␈α⊃coming␈α⊃from␈α∩observation␈α⊃of␈α⊃the␈α⊃world␈α∩with␈α⊃general
␈↓ ↓H␈↓premises␈α∞-␈α∞here␈α∞expressed␈α
as␈α∞axioms.␈α∞ The␈α∞problem␈α∞chosen␈α
was␈α∞in␈α∞retrospective␈α∞chess␈α∞analysis␈α
-
␈↓ ↓H␈↓determining␈α
what␈α
piece␈α
fell␈α
o≥␈α∞the␈α
board␈α
in␈α
a␈α
chess␈α
position,␈α∞given␈α
that␈α
the␈α
position␈α
arose␈α∞in␈α
a
␈↓ ↓H␈↓legal␈α
game␈α
of␈α
chess.␈α
The␈αreasoning␈α
involved␈α
di≥ers␈α
in␈α
many␈αsubtle␈α
ways␈α
from␈α
that␈α
involved␈αin
␈↓ ↓H␈↓the proof of a mathematical theorem.
␈↓ ↓H␈↓ Filman␈αhas␈αdone␈αan␈αexcellent␈αjob␈αof␈αformalizing␈αthis␈αreasoning␈αto␈αthe␈αextent␈αthat␈αthe␈αproof
␈↓ ↓H␈↓can␈α∞be␈α∞generated␈α∂and␈α∞checked␈α∞using␈α∂FOL,␈α∞our␈α∞≡rst␈α∞order␈α∂logic␈α∞interactive␈α∞theorem␈α∂prover␈α∞and
␈↓ ↓H␈↓proof␈α
checker.␈α
In␈α
the␈α
course␈α
of␈α
this,␈αhe␈α
has␈α
made␈α
many␈α
improvements␈α
to␈α
FOL,␈α
necessitated␈αby␈α
the
␈↓ ↓H␈↓fact␈α⊃that␈α⊂this␈α⊃was␈α⊂the␈α⊃largest␈α⊂task␈α⊃undertaken␈α⊂with␈α⊃FOL␈α⊂and␈α⊃used␈α⊂many␈α⊃previously␈α⊂untested
␈↓ ↓H␈↓features.␈α⊃ He␈α∩has␈α⊃exhibited␈α∩a␈α⊃high␈α∩degree␈α⊃of␈α⊃originality␈α∩in␈α⊃deciding␈α∩how␈α⊃to␈α∩translate␈α⊃vague
␈↓ ↓H␈↓informal␈α↔concepts␈α↔into␈α↔a␈α↔precise␈α↔mathematical␈α↔formalism.␈α↔ The␈α↔work␈α↔also␈α_required␈α↔great
␈↓ ↓H␈↓perseverance,␈αand␈αFilman␈αhas␈αshown␈αit␈αin␈αcompleting␈αhis␈αthesis␈αless␈αthan␈αthree␈αyears␈αof␈αgraduate
␈↓ ↓H␈↓work at Stanford.
␈↓ ↓H␈↓αProf. David Young␈↓ ¬\January 23, 1979␈↓
nPage 2␈↓
␈↓ ↓H␈↓ Filman␈α∞has␈α∞given␈α
numerous␈α∞presentations␈α∞of␈α
his␈α∞work␈α∞and␈α
served␈α∞as␈α∞a␈α∞teaching␈α
assistant.
␈↓ ↓H␈↓His␈αoral␈αpresentation␈αis␈αalso␈αexcellent,␈αand␈αI␈αexpect␈αhim␈αto␈αbe␈αan␈αexcellent␈αteacher.␈α He␈αalso␈αhas␈αa
␈↓ ↓H␈↓co-operative and pleasant personality.
␈↓ ↓H␈↓Sincerely,
␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305
␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ pJanuary 23, 1979
␈↓ ↓H␈↓Professor Michael A. Arbib
␈↓ ↓H␈↓Chairman of the Personnel Committee
␈↓ ↓H␈↓Department of Computer and Information Science
␈↓ ↓H␈↓Graduate Research Center
␈↓ ↓H␈↓University of Massachusetts
␈↓ ↓H␈↓Amherst Massachusetts 01003
␈↓ ↓H␈↓Dear Professor Arbib:
␈↓ ↓H␈↓ Robert␈αFilman␈αhas␈αjust␈αcompleted␈αhis␈αPhD␈αdissertation␈αunder␈αmy␈αdirection,␈αand␈αit␈αis␈αin␈αthe
␈↓ ↓H␈↓hands␈α
of␈αthe␈α
readers.␈α He␈α
has␈α
just␈αpassed␈α
his␈α≡nal␈α
oral␈α
examination,␈αand␈α
I␈αexpect␈α
him␈αto␈α
complete
␈↓ ↓H␈↓all work for his PhD in Winter Quarter or Spring Quarter at the latest.
␈↓ ↓H␈↓ His␈αthesis␈α
opens␈αa␈α
new␈αpart␈αof␈α
the␈αepistemology␈α
of␈αarti≡cial␈α
intelligence␈α-␈αstudying␈α
reasoning
␈↓ ↓H␈↓that␈αcombines␈αinference␈αand␈αobservation.␈α To␈αmy␈αknowledge␈αthis␈αis␈αthe␈α≡rst␈αresearch␈αpaper␈αin␈αthe
␈↓ ↓H␈↓area.
␈↓ ↓H␈↓ Its␈αimportance␈α
comes␈αfrom␈αthe␈α
fact␈αthat␈αmuch␈α
human␈αreasoning␈αdoes␈α
not␈αfollow␈α
the␈αmodel
␈↓ ↓H␈↓of␈α⊃pure␈α⊃mathematics␈α⊃but␈α∩combines␈α⊃facts␈α⊃coming␈α⊃from␈α∩observation␈α⊃of␈α⊃the␈α⊃world␈α∩with␈α⊃general
␈↓ ↓H␈↓premises␈α∞-␈α∞here␈α∞expressed␈α
as␈α∞axioms.␈α∞ The␈α∞problem␈α∞chosen␈α
was␈α∞in␈α∞retrospective␈α∞chess␈α∞analysis␈α
-
␈↓ ↓H␈↓determining␈α
what␈α
piece␈α
fell␈α
o≥␈α∞the␈α
board␈α
in␈α
a␈α
chess␈α
position,␈α∞given␈α
that␈α
the␈α
position␈α
arose␈α∞in␈α
a
␈↓ ↓H␈↓legal␈α
game␈α
of␈α
chess.␈α
The␈αreasoning␈α
involved␈α
di≥ers␈α
in␈α
many␈αsubtle␈α
ways␈α
from␈α
that␈α
involved␈αin
␈↓ ↓H␈↓the proof of a mathematical theorem.
␈↓ ↓H␈↓ Filman␈αhas␈αdone␈αan␈αexcellent␈αjob␈αof␈αformalizing␈αthis␈αreasoning␈αto␈αthe␈αextent␈αthat␈αthe␈αproof
␈↓ ↓H␈↓can␈α∞be␈α∞generated␈α∂and␈α∞checked␈α∞using␈α∂FOL,␈α∞our␈α∞≡rst␈α∞order␈α∂logic␈α∞interactive␈α∞theorem␈α∂prover␈α∞and
␈↓ ↓H␈↓proof␈α
checker.␈α
In␈α
the␈α
course␈α
of␈α
this,␈αhe␈α
has␈α
made␈α
many␈α
improvements␈α
to␈α
FOL,␈α
necessitated␈αby␈α
the
␈↓ ↓H␈↓fact␈α⊃that␈α⊂this␈α⊃was␈α⊂the␈α⊃largest␈α⊂task␈α⊃undertaken␈α⊂with␈α⊃FOL␈α⊂and␈α⊃used␈α⊂many␈α⊃previously␈α⊂untested
␈↓ ↓H␈↓features.␈α⊃ He␈α∩has␈α⊃exhibited␈α∩a␈α⊃high␈α∩degree␈α⊃of␈α⊃originality␈α∩in␈α⊃deciding␈α∩how␈α⊃to␈α∩translate␈α⊃vague
␈↓ ↓H␈↓informal␈α↔concepts␈α↔into␈α↔a␈α↔precise␈α↔mathematical␈α↔formalism.␈α↔ The␈α↔work␈α↔also␈α_required␈α↔great
␈↓ ↓H␈↓perseverance,␈αand␈αFilman␈αhas␈αshown␈αit␈αin␈αcompleting␈αhis␈αthesis␈αless␈αthan␈αthree␈αyears␈αof␈αgraduate
␈↓ ↓H␈↓work at Stanford.
␈↓ ↓H␈↓αProfessor Michael A. Arbib␈↓ ¬\January 23, 1979␈↓
nPage 2␈↓
␈↓ ↓H␈↓ Filman␈α∞has␈α∞given␈α
numerous␈α∞presentations␈α∞of␈α
his␈α∞work␈α∞and␈α
served␈α∞as␈α∞a␈α∞teaching␈α
assistant.
␈↓ ↓H␈↓His␈αoral␈αpresentation␈αis␈αalso␈αexcellent,␈αand␈αI␈αexpect␈αhim␈αto␈αbe␈αan␈αexcellent␈αteacher.␈α He␈αalso␈αhas␈αa
␈↓ ↓H␈↓co-operative and pleasant personality.
␈↓ ↓H␈↓Sincerely,
␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305
␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ pJanuary 23, 1979
␈↓ ↓H␈↓Prof. Alan Perlis
␈↓ ↓H␈↓Chairman, Department of Computer Science
␈↓ ↓H␈↓Yale University
␈↓ ↓H␈↓New Haven, Conn 06520
␈↓ ↓H␈↓Dear Professor Perlis:
␈↓ ↓H␈↓ Robert␈αFilman␈αhas␈αjust␈αcompleted␈αhis␈αPhD␈αdissertation␈αunder␈αmy␈αdirection,␈αand␈αit␈αis␈αin␈αthe
␈↓ ↓H␈↓hands␈α
of␈αthe␈α
readers.␈α He␈α
has␈α
just␈αpassed␈α
his␈α≡nal␈α
oral␈α
examination,␈αand␈α
I␈αexpect␈α
him␈αto␈α
complete
␈↓ ↓H␈↓all work for his PhD in Winter Quarter or Spring Quarter at the latest.
␈↓ ↓H␈↓ His␈αthesis␈α
opens␈αa␈α
new␈αpart␈αof␈α
the␈αepistemology␈α
of␈αarti≡cial␈α
intelligence␈α-␈αstudying␈α
reasoning
␈↓ ↓H␈↓that␈αcombines␈αinference␈αand␈αobservation.␈α To␈αmy␈αknowledge␈αthis␈αis␈αthe␈α≡rst␈αresearch␈αpaper␈αin␈αthe
␈↓ ↓H␈↓area.
␈↓ ↓H␈↓ Its␈αimportance␈α
comes␈αfrom␈αthe␈α
fact␈αthat␈αmuch␈α
human␈αreasoning␈αdoes␈α
not␈αfollow␈α
the␈αmodel
␈↓ ↓H␈↓of␈α⊃pure␈α⊃mathematics␈α⊃but␈α∩combines␈α⊃facts␈α⊃coming␈α⊃from␈α∩observation␈α⊃of␈α⊃the␈α⊃world␈α∩with␈α⊃general
␈↓ ↓H␈↓premises␈α∞-␈α∞here␈α∞expressed␈α
as␈α∞axioms.␈α∞ The␈α∞problem␈α∞chosen␈α
was␈α∞in␈α∞retrospective␈α∞chess␈α∞analysis␈α
-
␈↓ ↓H␈↓determining␈α
what␈α
piece␈α
fell␈α
o≥␈α∞the␈α
board␈α
in␈α
a␈α
chess␈α
position,␈α∞given␈α
that␈α
the␈α
position␈α
arose␈α∞in␈α
a
␈↓ ↓H␈↓legal␈α
game␈α
of␈α
chess.␈α
The␈αreasoning␈α
involved␈α
di≥ers␈α
in␈α
many␈αsubtle␈α
ways␈α
from␈α
that␈α
involved␈αin
␈↓ ↓H␈↓the proof of a mathematical theorem.
␈↓ ↓H␈↓ Filman␈αhas␈αdone␈αan␈αexcellent␈αjob␈αof␈αformalizing␈αthis␈αreasoning␈αto␈αthe␈αextent␈αthat␈αthe␈αproof
␈↓ ↓H␈↓can␈α∞be␈α∞generated␈α∂and␈α∞checked␈α∞using␈α∂FOL,␈α∞our␈α∞≡rst␈α∞order␈α∂logic␈α∞interactive␈α∞theorem␈α∂prover␈α∞and
␈↓ ↓H␈↓proof␈α
checker.␈α
In␈α
the␈α
course␈α
of␈α
this,␈αhe␈α
has␈α
made␈α
many␈α
improvements␈α
to␈α
FOL,␈α
necessitated␈αby␈α
the
␈↓ ↓H␈↓fact␈α⊃that␈α⊂this␈α⊃was␈α⊂the␈α⊃largest␈α⊂task␈α⊃undertaken␈α⊂with␈α⊃FOL␈α⊂and␈α⊃used␈α⊂many␈α⊃previously␈α⊂untested
␈↓ ↓H␈↓features.␈α⊃ He␈α∩has␈α⊃exhibited␈α∩a␈α⊃high␈α∩degree␈α⊃of␈α⊃originality␈α∩in␈α⊃deciding␈α∩how␈α⊃to␈α∩translate␈α⊃vague
␈↓ ↓H␈↓informal␈α↔concepts␈α↔into␈α↔a␈α↔precise␈α↔mathematical␈α↔formalism.␈α↔ The␈α↔work␈α↔also␈α_required␈α↔great
␈↓ ↓H␈↓perseverance,␈αand␈αFilman␈αhas␈αshown␈αit␈αin␈αcompleting␈αhis␈αthesis␈αless␈αthan␈αthree␈αyears␈αof␈αgraduate
␈↓ ↓H␈↓work at Stanford.
␈↓ ↓H␈↓αProf. Alan Perlis␈↓ ¬\January 23, 1979␈↓
nPage 2␈↓
␈↓ ↓H␈↓ Filman␈α∞has␈α∞given␈α
numerous␈α∞presentations␈α∞of␈α
his␈α∞work␈α∞and␈α
served␈α∞as␈α∞a␈α∞teaching␈α
assistant.
␈↓ ↓H␈↓His␈αoral␈αpresentation␈αis␈αalso␈αexcellent,␈αand␈αI␈αexpect␈αhim␈αto␈αbe␈αan␈αexcellent␈αteacher.␈α He␈αalso␈αhas␈αa
␈↓ ↓H␈↓co-operative and pleasant personality.
␈↓ ↓H␈↓Sincerely,
␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305
␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ pJanuary 23, 1979
␈↓ ↓H␈↓Professor Lawrence H. Landweber
␈↓ ↓H␈↓Chairman, Computer Sciences Department
␈↓ ↓H␈↓University of Wisconsin - Madison
␈↓ ↓H␈↓1210 West Dayton Street
␈↓ ↓H␈↓Madison, Wisconsin 53706
␈↓ ↓H␈↓Dear Professor Landweber:
␈↓ ↓H␈↓ Robert␈αFilman␈αhas␈αjust␈αcompleted␈αhis␈αPhD␈αdissertation␈αunder␈αmy␈αdirection,␈αand␈αit␈αis␈αin␈αthe
␈↓ ↓H␈↓hands␈α
of␈αthe␈α
readers.␈α He␈α
has␈α
just␈αpassed␈α
his␈α≡nal␈α
oral␈α
examination,␈αand␈α
I␈αexpect␈α
him␈αto␈α
complete
␈↓ ↓H␈↓all work for his PhD in Winter Quarter or Spring Quarter at the latest.
␈↓ ↓H␈↓ His␈αthesis␈α
opens␈αa␈α
new␈αpart␈αof␈α
the␈αepistemology␈α
of␈αarti≡cial␈α
intelligence␈α-␈αstudying␈α
reasoning
␈↓ ↓H␈↓that␈αcombines␈αinference␈αand␈αobservation.␈α To␈αmy␈αknowledge␈αthis␈αis␈αthe␈α≡rst␈αresearch␈αpaper␈αin␈αthe
␈↓ ↓H␈↓area.
␈↓ ↓H␈↓ Its␈αimportance␈α
comes␈αfrom␈αthe␈α
fact␈αthat␈αmuch␈α
human␈αreasoning␈αdoes␈α
not␈αfollow␈α
the␈αmodel
␈↓ ↓H␈↓of␈α⊃pure␈α⊃mathematics␈α⊃but␈α∩combines␈α⊃facts␈α⊃coming␈α⊃from␈α∩observation␈α⊃of␈α⊃the␈α⊃world␈α∩with␈α⊃general
␈↓ ↓H␈↓premises␈α∞-␈α∞here␈α∞expressed␈α
as␈α∞axioms.␈α∞ The␈α∞problem␈α∞chosen␈α
was␈α∞in␈α∞retrospective␈α∞chess␈α∞analysis␈α
-
␈↓ ↓H␈↓determining␈α
what␈α
piece␈α
fell␈α
o≥␈α∞the␈α
board␈α
in␈α
a␈α
chess␈α
position,␈α∞given␈α
that␈α
the␈α
position␈α
arose␈α∞in␈α
a
␈↓ ↓H␈↓legal␈α
game␈α
of␈α
chess.␈α
The␈αreasoning␈α
involved␈α
di≥ers␈α
in␈α
many␈αsubtle␈α
ways␈α
from␈α
that␈α
involved␈αin
␈↓ ↓H␈↓the proof of a mathematical theorem.
␈↓ ↓H␈↓ Filman␈αhas␈αdone␈αan␈αexcellent␈αjob␈αof␈αformalizing␈αthis␈αreasoning␈αto␈αthe␈αextent␈αthat␈αthe␈αproof
␈↓ ↓H␈↓can␈α∞be␈α∞generated␈α∂and␈α∞checked␈α∞using␈α∂FOL,␈α∞our␈α∞≡rst␈α∞order␈α∂logic␈α∞interactive␈α∞theorem␈α∂prover␈α∞and
␈↓ ↓H␈↓proof␈α
checker.␈α
In␈α
the␈α
course␈α
of␈α
this,␈αhe␈α
has␈α
made␈α
many␈α
improvements␈α
to␈α
FOL,␈α
necessitated␈αby␈α
the
␈↓ ↓H␈↓fact␈α⊃that␈α⊂this␈α⊃was␈α⊂the␈α⊃largest␈α⊂task␈α⊃undertaken␈α⊂with␈α⊃FOL␈α⊂and␈α⊃used␈α⊂many␈α⊃previously␈α⊂untested
␈↓ ↓H␈↓features.␈α⊃ He␈α∩has␈α⊃exhibited␈α∩a␈α⊃high␈α∩degree␈α⊃of␈α⊃originality␈α∩in␈α⊃deciding␈α∩how␈α⊃to␈α∩translate␈α⊃vague
␈↓ ↓H␈↓informal␈α↔concepts␈α↔into␈α↔a␈α↔precise␈α↔mathematical␈α↔formalism.␈α↔ The␈α↔work␈α↔also␈α_required␈α↔great
␈↓ ↓H␈↓perseverance,␈αand␈αFilman␈αhas␈αshown␈αit␈αin␈αcompleting␈αhis␈αthesis␈αless␈αthan␈αthree␈αyears␈αof␈αgraduate
␈↓ ↓H␈↓work at Stanford.
␈↓ ↓H␈↓αProfessor Lawrence H. Landweber␈↓ ¬\January 23, 1979␈↓
nPage 2␈↓
␈↓ ↓H␈↓ Filman␈α∞has␈α∞given␈α
numerous␈α∞presentations␈α∞of␈α
his␈α∞work␈α∞and␈α
served␈α∞as␈α∞a␈α∞teaching␈α
assistant.
␈↓ ↓H␈↓His␈αoral␈αpresentation␈αis␈αalso␈αexcellent,␈αand␈αI␈αexpect␈αhim␈αto␈αbe␈αan␈αexcellent␈αteacher.␈α He␈αalso␈αhas␈αa
␈↓ ↓H␈↓co-operative and pleasant personality.
␈↓ ↓H␈↓Sincerely,
␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305
␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ pJanuary 23, 1979
␈↓ ↓H␈↓Professor Jack Minker
␈↓ ↓H␈↓Chairman, Department of Computer Science
␈↓ ↓H␈↓University of Maryland
␈↓ ↓H␈↓College Park, Maryland 20742
␈↓ ↓H␈↓Dear Jack:
␈↓ ↓H␈↓ Robert␈αFilman␈αhas␈αjust␈αcompleted␈αhis␈αPhD␈αdissertation␈αunder␈αmy␈αdirection,␈αand␈αit␈αis␈αin␈αthe
␈↓ ↓H␈↓hands␈α
of␈αthe␈α
readers.␈α He␈α
has␈α
just␈αpassed␈α
his␈α≡nal␈α
oral␈α
examination,␈αand␈α
I␈αexpect␈α
him␈αto␈α
complete
␈↓ ↓H␈↓all work for his PhD in Winter Quarter or Spring Quarter at the latest.
␈↓ ↓H␈↓ His␈αthesis␈α
opens␈αa␈α
new␈αpart␈αof␈α
the␈αepistemology␈α
of␈αarti≡cial␈α
intelligence␈α-␈αstudying␈α
reasoning
␈↓ ↓H␈↓that␈αcombines␈αinference␈αand␈αobservation.␈α To␈αmy␈αknowledge␈αthis␈αis␈αthe␈α≡rst␈αresearch␈αpaper␈αin␈αthe
␈↓ ↓H␈↓area.
␈↓ ↓H␈↓ Its␈αimportance␈α
comes␈αfrom␈αthe␈α
fact␈αthat␈αmuch␈α
human␈αreasoning␈αdoes␈α
not␈αfollow␈α
the␈αmodel
␈↓ ↓H␈↓of␈α⊃pure␈α⊃mathematics␈α⊃but␈α∩combines␈α⊃facts␈α⊃coming␈α⊃from␈α∩observation␈α⊃of␈α⊃the␈α⊃world␈α∩with␈α⊃general
␈↓ ↓H␈↓premises␈α∞-␈α∞here␈α∞expressed␈α
as␈α∞axioms.␈α∞ The␈α∞problem␈α∞chosen␈α
was␈α∞in␈α∞retrospective␈α∞chess␈α∞analysis␈α
-
␈↓ ↓H␈↓determining␈α
what␈α
piece␈α
fell␈α
o≥␈α∞the␈α
board␈α
in␈α
a␈α
chess␈α
position,␈α∞given␈α
that␈α
the␈α
position␈α
arose␈α∞in␈α
a
␈↓ ↓H␈↓legal␈α
game␈α
of␈α
chess.␈α
The␈αreasoning␈α
involved␈α
di≥ers␈α
in␈α
many␈αsubtle␈α
ways␈α
from␈α
that␈α
involved␈αin
␈↓ ↓H␈↓the proof of a mathematical theorem.
␈↓ ↓H␈↓ Filman␈αhas␈αdone␈αan␈αexcellent␈αjob␈αof␈αformalizing␈αthis␈αreasoning␈αto␈αthe␈αextent␈αthat␈αthe␈αproof
␈↓ ↓H␈↓can␈α∞be␈α∞generated␈α∂and␈α∞checked␈α∞using␈α∂FOL,␈α∞our␈α∞≡rst␈α∞order␈α∂logic␈α∞interactive␈α∞theorem␈α∂prover␈α∞and
␈↓ ↓H␈↓proof␈α
checker.␈α
In␈α
the␈α
course␈α
of␈α
this,␈αhe␈α
has␈α
made␈α
many␈α
improvements␈α
to␈α
FOL,␈α
necessitated␈αby␈α
the
␈↓ ↓H␈↓fact␈α⊃that␈α⊂this␈α⊃was␈α⊂the␈α⊃largest␈α⊂task␈α⊃undertaken␈α⊂with␈α⊃FOL␈α⊂and␈α⊃used␈α⊂many␈α⊃previously␈α⊂untested
␈↓ ↓H␈↓features.␈α⊃ He␈α∩has␈α⊃exhibited␈α∩a␈α⊃high␈α∩degree␈α⊃of␈α⊃originality␈α∩in␈α⊃deciding␈α∩how␈α⊃to␈α∩translate␈α⊃vague
␈↓ ↓H␈↓informal␈α↔concepts␈α↔into␈α↔a␈α↔precise␈α↔mathematical␈α↔formalism.␈α↔ The␈α↔work␈α↔also␈α_required␈α↔great
␈↓ ↓H␈↓perseverance,␈αand␈αFilman␈αhas␈αshown␈αit␈αin␈αcompleting␈αhis␈αthesis␈αless␈αthan␈αthree␈αyears␈αof␈αgraduate
␈↓ ↓H␈↓work at Stanford.
␈↓ ↓H␈↓αProfessor Jack Minker␈↓ ¬\January 23, 1979␈↓
nPage 2␈↓
␈↓ ↓H␈↓ Filman␈α∞has␈α∞given␈α
numerous␈α∞presentations␈α∞of␈α
his␈α∞work␈α∞and␈α
served␈α∞as␈α∞a␈α∞teaching␈α
assistant.
␈↓ ↓H␈↓His␈αoral␈αpresentation␈αis␈αalso␈αexcellent,␈αand␈αI␈αexpect␈αhim␈αto␈αbe␈αan␈αexcellent␈αteacher.␈α He␈αalso␈αhas␈αa
␈↓ ↓H␈↓co-operative and pleasant personality.
␈↓ ↓H␈↓Sincerely,
␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305
␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ pJanuary 23, 1979
␈↓ ↓H␈↓Prof. S.D. Conte
␈↓ ↓H␈↓Chairman, Department of Computer Science
␈↓ ↓H␈↓Mathematical Sciences Building; Room 442
␈↓ ↓H␈↓Purdue University
␈↓ ↓H␈↓West Lafayette, Indiana 47907
␈↓ ↓H␈↓Dear Professor Conte:
␈↓ ↓H␈↓ Robert␈αFilman␈αhas␈αjust␈αcompleted␈αhis␈αPhD␈αdissertation␈αunder␈αmy␈αdirection,␈αand␈αit␈αis␈αin␈αthe
␈↓ ↓H␈↓hands␈α
of␈αthe␈α
readers.␈α He␈α
has␈α
just␈αpassed␈α
his␈α≡nal␈α
oral␈α
examination,␈αand␈α
I␈αexpect␈α
him␈αto␈α
complete
␈↓ ↓H␈↓all work for his PhD in Winter Quarter or Spring Quarter at the latest.
␈↓ ↓H␈↓ His␈αthesis␈α
opens␈αa␈α
new␈αpart␈αof␈α
the␈αepistemology␈α
of␈αarti≡cial␈α
intelligence␈α-␈αstudying␈α
reasoning
␈↓ ↓H␈↓that␈αcombines␈αinference␈αand␈αobservation.␈α To␈αmy␈αknowledge␈αthis␈αis␈αthe␈α≡rst␈αresearch␈αpaper␈αin␈αthe
␈↓ ↓H␈↓area.
␈↓ ↓H␈↓ Its␈αimportance␈α
comes␈αfrom␈αthe␈α
fact␈αthat␈αmuch␈α
human␈αreasoning␈αdoes␈α
not␈αfollow␈α
the␈αmodel
␈↓ ↓H␈↓of␈α⊃pure␈α⊃mathematics␈α⊃but␈α∩combines␈α⊃facts␈α⊃coming␈α⊃from␈α∩observation␈α⊃of␈α⊃the␈α⊃world␈α∩with␈α⊃general
␈↓ ↓H␈↓premises␈α∞-␈α∞here␈α∞expressed␈α
as␈α∞axioms.␈α∞ The␈α∞problem␈α∞chosen␈α
was␈α∞in␈α∞retrospective␈α∞chess␈α∞analysis␈α
-
␈↓ ↓H␈↓determining␈α
what␈α
piece␈α
fell␈α
o≥␈α∞the␈α
board␈α
in␈α
a␈α
chess␈α
position,␈α∞given␈α
that␈α
the␈α
position␈α
arose␈α∞in␈α
a
␈↓ ↓H␈↓legal␈α
game␈α
of␈α
chess.␈α
The␈αreasoning␈α
involved␈α
di≥ers␈α
in␈α
many␈αsubtle␈α
ways␈α
from␈α
that␈α
involved␈αin
␈↓ ↓H␈↓the proof of a mathematical theorem.
␈↓ ↓H␈↓ Filman␈αhas␈αdone␈αan␈αexcellent␈αjob␈αof␈αformalizing␈αthis␈αreasoning␈αto␈αthe␈αextent␈αthat␈αthe␈αproof
␈↓ ↓H␈↓can␈α∞be␈α∞generated␈α∂and␈α∞checked␈α∞using␈α∂FOL,␈α∞our␈α∞≡rst␈α∞order␈α∂logic␈α∞interactive␈α∞theorem␈α∂prover␈α∞and
␈↓ ↓H␈↓proof␈α
checker.␈α
In␈α
the␈α
course␈α
of␈α
this,␈αhe␈α
has␈α
made␈α
many␈α
improvements␈α
to␈α
FOL,␈α
necessitated␈αby␈α
the
␈↓ ↓H␈↓fact␈α⊃that␈α⊂this␈α⊃was␈α⊂the␈α⊃largest␈α⊂task␈α⊃undertaken␈α⊂with␈α⊃FOL␈α⊂and␈α⊃used␈α⊂many␈α⊃previously␈α⊂untested
␈↓ ↓H␈↓features.␈α⊃ He␈α∩has␈α⊃exhibited␈α∩a␈α⊃high␈α∩degree␈α⊃of␈α⊃originality␈α∩in␈α⊃deciding␈α∩how␈α⊃to␈α∩translate␈α⊃vague
␈↓ ↓H␈↓informal␈α↔concepts␈α↔into␈α↔a␈α↔precise␈α↔mathematical␈α↔formalism.␈α↔ The␈α↔work␈α↔also␈α_required␈α↔great
␈↓ ↓H␈↓perseverance,␈αand␈αFilman␈αhas␈αshown␈αit␈αin␈αcompleting␈αhis␈αthesis␈αless␈αthan␈αthree␈αyears␈αof␈αgraduate
␈↓ ↓H␈↓work at Stanford.
␈↓ ↓H␈↓αProf. S.D. Conte␈↓ ¬\January 23, 1979␈↓
nPage 2␈↓
␈↓ ↓H␈↓ Filman␈α∞has␈α∞given␈α
numerous␈α∞presentations␈α∞of␈α
his␈α∞work␈α∞and␈α
served␈α∞as␈α∞a␈α∞teaching␈α
assistant.
␈↓ ↓H␈↓His␈αoral␈αpresentation␈αis␈αalso␈αexcellent,␈αand␈αI␈αexpect␈αhim␈αto␈αbe␈αan␈αexcellent␈αteacher.␈α He␈αalso␈αhas␈αa
␈↓ ↓H␈↓co-operative and pleasant personality.
␈↓ ↓H␈↓Sincerely,
␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305
␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ pJanuary 23, 1979
␈↓ ↓H␈↓Mr. Sidney L. Mantler
␈↓ ↓H␈↓Thomas J. Watson Research Center
␈↓ ↓H␈↓P.O. Box 218
␈↓ ↓H␈↓Yorktown Heights, New York 10598
␈↓ ↓H␈↓Dear Mr. Mantler:
␈↓ ↓H␈↓ Robert␈αFilman␈αhas␈αjust␈αcompleted␈αhis␈αPhD␈αdissertation␈αunder␈αmy␈αdirection,␈αand␈αit␈αis␈αin␈αthe
␈↓ ↓H␈↓hands␈α
of␈αthe␈α
readers.␈α He␈α
has␈α
just␈αpassed␈α
his␈α≡nal␈α
oral␈α
examination,␈αand␈α
I␈αexpect␈α
him␈αto␈α
complete
␈↓ ↓H␈↓all work for his PhD in Winter Quarter or Spring Quarter at the latest.
␈↓ ↓H␈↓ His␈αthesis␈α
opens␈αa␈α
new␈αpart␈αof␈α
the␈αepistemology␈α
of␈αarti≡cial␈α
intelligence␈α-␈αstudying␈α
reasoning
␈↓ ↓H␈↓that␈αcombines␈αinference␈αand␈αobservation.␈α To␈αmy␈αknowledge␈αthis␈αis␈αthe␈α≡rst␈αresearch␈αpaper␈αin␈αthe
␈↓ ↓H␈↓area.
␈↓ ↓H␈↓ Its␈αimportance␈α
comes␈αfrom␈αthe␈α
fact␈αthat␈αmuch␈α
human␈αreasoning␈αdoes␈α
not␈αfollow␈α
the␈αmodel
␈↓ ↓H␈↓of␈α⊃pure␈α⊃mathematics␈α⊃but␈α∩combines␈α⊃facts␈α⊃coming␈α⊃from␈α∩observation␈α⊃of␈α⊃the␈α⊃world␈α∩with␈α⊃general
␈↓ ↓H␈↓premises␈α∞-␈α∞here␈α∞expressed␈α
as␈α∞axioms.␈α∞ The␈α∞problem␈α∞chosen␈α
was␈α∞in␈α∞retrospective␈α∞chess␈α∞analysis␈α
-
␈↓ ↓H␈↓determining␈α
what␈α
piece␈α
fell␈α
o≥␈α∞the␈α
board␈α
in␈α
a␈α
chess␈α
position,␈α∞given␈α
that␈α
the␈α
position␈α
arose␈α∞in␈α
a
␈↓ ↓H␈↓legal␈α
game␈α
of␈α
chess.␈α
The␈αreasoning␈α
involved␈α
di≥ers␈α
in␈α
many␈αsubtle␈α
ways␈α
from␈α
that␈α
involved␈αin
␈↓ ↓H␈↓the proof of a mathematical theorem.
␈↓ ↓H␈↓ Filman␈αhas␈αdone␈αan␈αexcellent␈αjob␈αof␈αformalizing␈αthis␈αreasoning␈αto␈αthe␈αextent␈αthat␈αthe␈αproof
␈↓ ↓H␈↓can␈α∞be␈α∞generated␈α∂and␈α∞checked␈α∞using␈α∂FOL,␈α∞our␈α∞≡rst␈α∞order␈α∂logic␈α∞interactive␈α∞theorem␈α∂prover␈α∞and
␈↓ ↓H␈↓proof␈α
checker.␈α
In␈α
the␈α
course␈α
of␈α
this,␈αhe␈α
has␈α
made␈α
many␈α
improvements␈α
to␈α
FOL,␈α
necessitated␈αby␈α
the
␈↓ ↓H␈↓fact␈α⊃that␈α⊂this␈α⊃was␈α⊂the␈α⊃largest␈α⊂task␈α⊃undertaken␈α⊂with␈α⊃FOL␈α⊂and␈α⊃used␈α⊂many␈α⊃previously␈α⊂untested
␈↓ ↓H␈↓features.␈α⊃ He␈α∩has␈α⊃exhibited␈α∩a␈α⊃high␈α∩degree␈α⊃of␈α⊃originality␈α∩in␈α⊃deciding␈α∩how␈α⊃to␈α∩translate␈α⊃vague
␈↓ ↓H␈↓informal␈α↔concepts␈α↔into␈α↔a␈α↔precise␈α↔mathematical␈α↔formalism.␈α↔ The␈α↔work␈α↔also␈α_required␈α↔great
␈↓ ↓H␈↓perseverance,␈αand␈αFilman␈αhas␈αshown␈αit␈αin␈αcompleting␈αhis␈αthesis␈αless␈αthan␈αthree␈αyears␈αof␈αgraduate
␈↓ ↓H␈↓work at Stanford.
␈↓ ↓H␈↓αMr. Sidney L. Mantler␈↓ ¬\January 23, 1979␈↓
nPage 2␈↓
␈↓ ↓H␈↓ Filman␈α∞has␈α∞given␈α
numerous␈α∞presentations␈α∞of␈α
his␈α∞work␈α∞and␈α
served␈α∞as␈α∞a␈α∞teaching␈α
assistant.
␈↓ ↓H␈↓His␈αoral␈αpresentation␈αis␈αalso␈αexcellent,␈αand␈αI␈αexpect␈αhim␈αto␈αbe␈αan␈αexcellent␈αteacher.␈α He␈αalso␈αhas␈αa
␈↓ ↓H␈↓co-operative and pleasant personality.
␈↓ ↓H␈↓Sincerely,
␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science